T:Type, as:(T List), f,g:(T).
subtype_rel(T; )
 sorted(as)
 no_repeats(T; as)
 ((priority-select(f; g; as) = (inl tt )  (?))
  l_exists(as; T; a.(((f(a)))  (b:T. (b  as)  (b < a)  (((g(b)))))))) 

latex

Definitions	P  Q, x:A. B(x), sorted(L), l_exists(L; T; x.P(x)), t  T, x:A. B(x), b, A, prop{i:l}, P  Q, (x  l), x. t(x), P  Q, int_seg(i; j), False, ||as||, lelt(i; j; k), A  B, l[i], P  Q, Unit, tt, priority-select(f; g; as), , subtype(S; T), no_repeats(T; l), , P  Q, decidable(P), A c B, guard(T), sq_type(T)
Lemmas	decidable int equal, strict-sorted, le wf, decidable lt, select member, no repeats wf, sorted wf, priority-select-property, iff functionality wrt iff, bool wf, priority-select wf, btrue wf, unit wf, int seg wf, select wf, length wf1, l exists wf, l member wf, not wf, assert wf